Inference at * 2 0 
Iof proof for Lemma before last:



1. T : Type
2. T List
3. u : T
4. v : T List
5. x:T. (x  v)  ((x = last(v)))  x before last(v)  v
  x:T. (x  [u / v])  ((x = last([u / v])))  x before last([u / v])  [u / v] 

latex

 by InteriorProof PERMUTE{1:n,
 by InteriorProof PERMUTE{2:n,
 by InteriorProof PERMUTE{1:n,
 by InteriorProof PERMUTE{2:n,
 by InteriorProof PERMUTE{2:n,
 by InteriorProof PERMUTE{3:n,
 by InteriorProof PERMUTE{4:n,
 by InteriorProof PERMUTE{3:n,
 by InteriorProof PERMUTE{4:n,
 by InteriorProof PERMUTE{4:n,
 by InteriorProof PERMUTE{3:n,
 by InteriorProof PERMUTE{3:n,
 by InteriorProof PERMUTE{3:n,
 by InteriorProof PERMUTE{3:n,
 by InteriorProof PERMUTE{3:n,
 by InteriorProof PERMUTE{3:n,
 by InteriorProof PERMUTE{5:n,
 by InteriorProof PERMUTE{6:n,
 by InteriorProof PERMUTE{6:n,
 by InteriorProof PERMUTE{3:n,
 by InteriorProof PERMUTE{4:n,
 by InteriorProof PERMUTE{4:n,
 by InteriorProof PERMUTE{7:n,
 by InteriorProof PERMUTE{5:n} 

latex

 1: 

 1: 6. x : T
 1: 7. (x  [u / v])
 1:   (null([u / v]))
 2: 

 2: 6. x : T
 2: 7. (x  [u / v])
 2: 8. (x = last([u / v]))
 2:   (null([u / v]))
 3: 

 3: 6. T
 3:   (null([u / v]))
 4: 

 4: 6. x : T
 4: 7. (x = last([u / v]))
 4:   (null([u / v]))
 5: 

 5: 6. x : T
 5: 7. (x = u)  (x  v)
 5:   (null([u / v]))
 6: 

 6: 6. x : T
 6: 7. (x = u)  (x  v)
 6: 8. (x = last([u / v]))
 6:   (null([u / v]))
 7: 

 7: 6. x : T
 7: 7. (x = u)  (x  v)
 7: 8. (x = last([u / v]))
 7:   (x = u & [last([u / v])]  v)  [x; last([u / v])]  v
 .

Definitions	x:A  B(x), left + right, null(as), b, f(a), [], L1  L2, [car / cdr], x.A(x), x:AB(x), last(L), s = t, A, (x  l), type List, Type, {T}, x(s), x before y  l, x. t(x), P  Q, P  Q, P & Q, P  Q, , t  T, P  Q, x:A. B(x)
Lemmas	cons sublist cons, cons member, implies functionality wrt iff, all functionality wrt iff, sublist wf, last wf, not wf, l member wf